Formal methods
Formal methods are mathematical techniques for developing computer-based software and hardware systems. __TOC__ Please update this page or add a new page if you know of relevant online information not included here or would like to maintain information on a particular topic. Use the [http://groups.google.com/group/comp.specification.misc comp.specification.misc] newsgroup, for general formal methods queries. Please link to http://formalmethods.wikia.com if you create a permanent hyperlink to this website. In case of problems, please contact Jonathan Bowen. ---- Introduction This document contains some pointers to information on , useful for mathematically describing and reasoning about computer-based systems, available around the world on the World Wide Web (WWW). Formal methods are a fault avoidance technique that help in the reduction of errors introduced into a system, particularly at the earlier stages of design. They complement fault removal techniques like testing. Links for accessing online information in the following categories are available: * Announcement * Selected resources * Introductory articles * Individual notations, methods and tools * Publications (journals, papers, books, etc.) * Electronic repositories * Education resources * Meetings * Projects * Companies * Organizations * Who's who * Selected photographs * Newsgroups and mailing lists * Safety-critical systems * Related topics indicates new entries. indicates a (subjectively!) recommended link for especially good online information. Selected resources This space will be used to indicate selected new entries and developments in these formal methods pages. * Formal Methods authors on . (30 November 2011) * Wikified and moved to formalmethods.wikia.com. (10 March 2009) * Formal methods entries in the Wikipedia encyclopedia (30 October 2005) * The preferred and stable URL for the Virtual Library formal methods pages is now http://vl.fmnet.info. (30 November 2004) * Checked and updated main links to formal methods. (22 April 2001) * Moved to the Centre for Applied Formal Methods, . (13 January 2001) * New [http://www.iist.unu.edu/dc/ Duration Calculus and RAISE pages. (31 July 1999 / 17 August 1999) * New education resources section by Kathi Fisler added. (23 February 1999) * Search for newsgroup articles on formal methods in Google Groups. (19 December 1997) * Some Formal Methods Humour. (25 September 1997) * FM'99: The World Congress on Formal Methods, 20-24 September 1999. (24 July 1997) * Photographs from the 1st B Conference, Nantes, France, 25–27 November 1996. (6 December 1996) * Strategic Directions in Computing Research Formal Methods Working Group, ACM, USA. (16 September 1996) * B-Core (UK) Ltd are now on-line. (25 June 1996) * EVES and Z/EVES are now available for on-line distribution. (25 June 1996) * The Steam Boiler Control Specification Problem by J.-R. Abrial, E. Börger and H. Langmaack. A comparative case study for different formal techniques. Published as LNCS 1165. (2 August 1995) * [http://groups.google.com/group/comp.specification.misc Comp.specification.misc] newsgroup. (12 July 1995) * Petri Nets graphical notation. (11 April 1995) * Tools demonstration information for WIFT95 workshop. (6 April 1995) * A new LOTOS page. (16 February 1995) * Information on RAISE language and tools. (19 January 1995, updated 17 August 1999) * A new section on the B-Method has been added. (6 January 1995) ---- Individual notations, methods and tools # Abstract State Machines (ASM). Formerly known as Evolving Algebras. # ACL2 (A Computational Logic for Applicative Common Lisp) theorem prover, a successor to the Nqthm Boyer-Moore theorem prover. # ACSR (Algebra of Communicating Shared Resources) and Graphical Communicating Shared Resources (GCSR), a formal language for the specification, refinement, and analysis of real-time systems. See the tools VERSA (Verification Execution and Rewrite System for ACSR) and PARAGON for visual specification and verification of real-time systems. # Action Semantics, a framework for specifying formal semantics of programming languages. # Action systems for reasoning about distributed systems. # aiT WCET Analyzer, an abstract interpretation based static analyzer that computes safe upper bounds for the worst-case execution time of tasks. # Alloy Analyzer, an object modelling notation that is compatible with development approaches such as UML, Catalysis, Fusion, OMT and Syntropy, strongly influenced by the Z specification language. See Alloy discussion group. # Algebraic Design Language, a higher-order software specification language. # Argos, an imperative synchronous language with verification support. # Assertion Definition Language (ADL), a specification based testing toolset. # Astrée, an abstract interpretation based static analyzer that proves the absence of runtime errors in C programs. # Autofocus for specifying distributed systems. First prize winner in the tool competition at FM'99. # BDDs (Binary Decision Diagrams) for finite-state verification problems. # B-Method, including the B-Tool and B-Toolkit. # Boyer-Moore theorem prover (a forerunner of Nqthm and ACL2). Available via ICOT Free Software for use under Unix at ICOT (Japan). # CADP: a widespread toolbox for the Construction and Analysis of Distributed Processes, developed at INRIA Grenoble # CASL: Common Algebraic Specification Language, for algebraic specification and development, from CoFI, the Common Framework Initiative. # CafeOBJ, an algebraic specification and programming language. A successor of OBJ. # CCS (Calculus of Communicating Systems). A process algebra for concurrent systems. # Circal (CIRcuit CALculus) System supporting a process algebra which may be used to rigorously describe, verify and simulate concurrent systems. See software. # CLaReT: The Computer Language Reasoning Tool. # COLD (Common Object-oriented Language for Design), a wide-spectrum specification language. # CommUnity, based on category theory. See also CommUnity Workbench. # Concurrency Factory, a "next generation" Concurrency Workbench toolkit. # Coq proof assistant: checks proofs about assertions, helps to find formal proofs and extracts certified programs from constructive proofs. # CSP (Communicating Sequential Processes) including the FDR2 (Failures-Divergence Refinement) tool. # CWB Concurrency Factory and CWB-NC (The Concurrency Workbench of North Carolina), which includes a LOTOS interface, diagnostic information, etc. Note: The CWB and CWB-NC have a common ancestor, but are each under separate development. # dL -- differential dynamic logic for hybrid systems verification. # DisCo specification method for reactive systems including an animation tool, Finland. # Duration Calculus (DC), an interval logic for real-time systems. # ESC/Java2 Extended Static Checker for Java tool, using program verification technology. See also JML. # Escher C Verifier, a tool for formal verification of embedded software written in MISRA-C. # Estelle Formal Description Technique (IS 9074). See also EDT (Estelle Development Toolset). # Esterel language and tools for synchronous reactive systems. # EVES tool, based on ZF set theory, from ORA, Canada. See also Z/EVES which provides a Z notation front-end to EVES. # Extended ML framework for the specification and formal development of modular Standard ML programs. # FermaT program transformation system. See also here. # FormalCheck model checker tool for verifying the functionality of digital hardware designs in Verilog or VHDL, based on the COSPAN model checker. # HOL mechanical theorem proving system, based on Higher Order Logic. # HyTech (The HYbrid TECHnology Tool), an automatic tool for the analysis of embedded systems which computes the condition under which a linear hybrid system satisfies a temporal-logic requirement. # IMPS, an Interactive Mathematical Proof System intended to provide mechanical support for traditional mathematical techniques and styles of practice. # Interval Temporal Logic (ITL). See also and Temporal and Logic publications. # Isabelle, a generic theorem prover, supporting higher-order logic, ZF set theory, etc. # Jape (Just Another Proof Editor). A framework for building interactive proof editors. # JML (Java Modeling Language), a behavioral interface specification language for Java. See also ESC/Java2. # KeY An automatic and interactive, verification and test generation tool for Java Card. # KeYmaera A Hybrid Theorem Prover for Hybrid Systems. # KIV (Karlsruhe Interactive Verifier). A tool for the development of correct software using stepwise refinement. # Kronos, a verification tool for safety and liveness properties of real-time systems. Uses timed automata, TCTL (an extension of temporal logic) and model-checking. # Larch family of languages and tools supporting a two-tiered definitional style of specification. See especially LP, the Larch Prover. # LeanTAP, a tableau-based deduction theorem prover for classical first-order logic. # LEGO proof assistant. # Leo-II resolution-based automated theorem prover for Higher-Order Logic # LOTOS (Language of Temporal Ordering Specifications). # LPV Linear Programming based software Validation technology, including proofs and testing. # Lustre synchronous declarative language for programming reactive systems, including verification. # MALPAS static analysis tool-set. # Maintainer's Assistant, a tool for reverse engineering and re-engineering code using formal methods. # MathSpad structure editor, especially for mathematical calculations. # Maude system for equational and rewriting logic specification and programming. Influenced by OBJ3. # Meije tools for the verification of concurrent programs. Includes ATG, a graphical editor/visualizer. # μCRL (micro CRL), process algebraic language for communicating processes with data. # mCRL2 a toolset for a process algebraic language and a modal logic with data and time. Successor of μCRL. # Mizar System, a long-term effort aimed at developing software to support a working mathematician in preparing papers. See also here. # Model checking at CMU, a method for formally verifying finite-state concurrent systems. Available packages include: #* BDD library with extensions for sequential verification. #* CV, a VHDL model checker. #* CSML and MCB, a language for compositional description of finite state machines and a (non-symbolic) model checker for CTL. #* SMV (Symbolic Model Verifier) model checker for finite-state systems, using the specification language CTL (Computation Tree Logic), a propositional branching-time temporal logic. See also Word-level SMV for verifying arithmetic circuits efficiently. See also NuSMV, a new symbolic model checker. # Murphi description language and verifier tool for finite-state verification of concurrent systems. # Nqthm 1992, the latest Boyer-Moore theorem prover. Also accessible via FTP. Includes the Pc-Nqthm interactive Proof-checker. # Nuprl tool based on intuitionistic type theory. # OBJ family — OBJ3, 2OBJ, CafeOBJ, etc. Term rewriting and algebraic specification. # OCL (Object Constraint Language), part of UML. # Otter, an automated deduction system. # PEPA, a stochastic process algebra used for modelling systems composed of concurrently active components that co-operate and share work. # Perfect Developer tool from Escher Techologies Limited. # Petri Nets, a formal graphical notation for modelling systems with concurrency. See also here. # Pi-calculus: calculi for mobile processes. See also the Mobility Workbench and a searchable bibliography. # Pobl. A development method for concurrent object-based programs. # ProofPower is a commercial tool, developed by ICL, supporting development and checking of specifications and formal proofs in Higher Order Logic and/or Z. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z. # Prover Technology, commercial proof engines. # PVS (Prototype Verification System) language and tool based on classical typed higher-order logic. # RAISE (Rigorous Approach to Industrial Software Engineering). Includes RSL (RAISE Specification Language). # Rapide language and toolset, for building large-scale distributed multi-language systems. # Refinement Calculus, a formalisation of the stepwise refinement method of program construction. # RISC ProgramExplorer, a computer-supported program reasoning environment for educational purposes. # SCR (Software Cost Reduction), a tabular notation for specifying requirements and tools for creating and analyzing requirements specifications. # SDL (Specification and Description Language) from the SDL Forum Society. See also previous site here. # Signal/Polychrony language and toolset for synchronous systems. See also the related Esterel and Lustre. # SPARK (now AltranPraxis) secure subset of Ada, including the SPADE static analysis toolset. # Spec#, an extension of the C# programming language from Microsoft Research with specification features allowing static analysis using a program verifier. # Specware automated software development system for stepwise refinement of provably correct code. See also technology transfer information and publication from the Kestrel Institute. # SPIN is an automated verification tool (model checker), using PROMELA (PROcess MEta LAnguage), a language loosely based on CSP, for finite state systems, such as protocols or validation models of distributed systems, developed at Bell Laboratories. See also p2b, a translation utility. # StackAnalyzer, an abstract interpretation based static analyzer for computing the worst-case stack usage of tasks. # StateSim simulator for Statecharts models. Draw your models in Open Office Draw and the run your simulations from StateSim. # Statestep finite state machine modelling with comprehensive elicitation of unusual scenarios (addressing "corner cases" or the feature interaction problem). # STeP, the Stanford Temporal Prover. # TAM'97 (Trace Assertion Method). A formal method for abstract specification of module interfaces. # Temporal-Rover — formal specification and testing tool based on temporal logic. # TLA (Temporal Logic of Actions), a logic for specifying and reasoning about concurrent and reactive systems. # TPS and ETPS, the Theorem Proving System and the Educational Theorem Proving System. # TRIO language and tools for real-time systems, based on temporal logic. # TTM/RTTL framework for real-time reactive systems. # UNITY, a programming notation and a logic to reason about parallel and distributed programs. # UPPAAL verification and validation tools for real-time systems. Model checking and simulation with a graphical interface. # VCC, Microsoft Research - Verification of Concurrent C; a sound deductive verifier for C. # VeriSoft, Bell Laboratories, Lucent Technologies. A model checking tool for systematic software testing of concurrent/reactive/real-time systems. Automatically searches for coordination problems (deadlocks, etc.) and assertion violations. Supports C, C++, etc. # VDM (Vienna Development Method). See also Overture toolset. # VIS (Verification Interacting with Synthesis), a system for formal verification, synthesis, and simulation of finite state systems, especially logic circuits. Includes a Verilog HDL front-end. # X-machines, related to finite state machines. # Z notation for formal specification and extensions eg. TCOZ (Timed Communicating Object Z) . See also: * Formal methods entry and category in the Wikipedia free online encyclopedia. * Formal Methods Europe (FME) HUB. * Formal Methods Education Resources: Tool Pages. * Formal Verification Methods and Tools from the VERIMAG research group, France. * Formal verification Tools list from David Mentre, Association Gulliver. Newsgroups and mailing lists * [http://groups.google.com/group/comp.specification.misc Comp.specification.misc] newsgroup including discussion of formal specification and methods, and other related newsgroups (see [http://www.liszt.com/news/search.cgi?word=comp.specification comp.specification newsgroups] and here if you have news access problems): ** [http://groups.google.com/group/comp.specification.larch Comp.specification.larch] — more specific discussion on the Larch, now an archive. ** [http://groups.google.com/group/comp.specification.z Comp.specification.z] — more specific discussion on the Z and related notations. See monthly FAQ message (Frequently Asked Questions). * [http://groups.google.com/group/comp.software-eng Comp.software-eng] — general discussion on software engineering, including formal aspects. See also the [http://www.qucis.queensu.ca/Software-Engineering/ comp.software-eng Software Engineering Archives] and FAQ message information especially formal specification. * [http://groups.google.com/groups/news.announce.conferences News.announce.conferences] — announcements of conferences including many specifically on formal methods or with a formal methods content; e.g., see separate page on meetings. * Search for newsgroup articles on formal methods in Google Groups. The following electronic mailing lists cover general issues concerning formal methods: * ProCoS mailing list. FMnet, maintained by Jonathan Bowen. * ProCoS mailing list. Provably Correct Systems, maintained by Jonathan Bowen. There are a significant number of mailing lists concerning individual formal methods. Please see the relevant pages for the formal methods of interest for details. Of related interest See also information on: * Concurrent systems * Logic programming * Safety-critical systems * Computational logic * BNF (Backus-Naur Form notation) * Formal Methods from BRICS * Some Formal Methods Humor * David Crocker's Formal Verification blog * Words expressing abstract relations from Roget's Thesaurus — could be useful in describing formal specifications! * Theory of computation sites and other computing sites * Formal Methods links from Links2Go * UML (Unified Modeling Language) — see also: ** Resource page from OMG (Object Management Group) ** 2U Consortium (Unambiguous UML) ** pUML (Precise UML group) ** Google Directory links * Statecharts by David Harel * Synchronous Applications, Languages and Programs * TPTP Thousands of Problems for Theorem Provers * Logical frameworks * Cleanroom Software Engineering * Automated reasoning systems (see also systems developed in Germany) Cited in W.W. Gibbs, Software's Chronic Crisis, [http://www.sciam.com/ Scientific American], 271(3):86-95, September 1994. See also FormalMethods.com. :-) ---- Last updated by Jonathan Bowen, 2 August 2018. Further information for possible inclusion is welcome. Category:Content Category:Formal methods Category:Virtual Library